A:Type, eq:EqDecider(A), f,g:fpf(A; a.top), x:A.
(fpf-dom(eq; x; fpf-join(eq; f; g)))  ((fpf-dom(eq; x; f))  (fpf-dom(eq; x; g))) 

latex

Definitions	x:A. B(x), t  T, x. t(x), x(s)
Lemmas	fpf-join-dom, top wf, fpf wf, deq wf